T:Type, L,L1,L2:(T List).
(((null(L)))  ((last(L)  L2)))  sublist(T; L; append(L1; L2))  sublist(T; L; L1) 

latex

Definitions	prop{i:l}, t  T, P  Q, x:A. B(x), True, sublist(T; L1; L2), False, A  B, P  Q, lelt(i; j; k), A, int_seg(i; j), A c B, x:A. B(x), (x  l), P  Q, P  Q, suptype(S; T), subtype(S; T), , P  Q, decidable(P), guard(T), last(L)
Lemmas	last wf, l member wf, null wf, assert wf, not wf, append wf, sublist wf, decidable assert, nil sublist, assert of null, non nil length, not functionality wrt iff, int seg wf, le wf, length wf1, decidable lt, select wf, length append, non neg length, select append back, increasing implies le, increasing wf, select append front